$\forall$${\it es}$:ES, ${\it dom}$:(E$\rightarrow\mathbb{B}$).
\\[0ex]($\forall$$e$:E. ($\uparrow$isrcv($e$)) $\Rightarrow$ ($\neg$($\uparrow$(${\it dom}$(sender($e$))))) $\Rightarrow$ ($\uparrow$isrcv(sender($e$))))
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. ($\uparrow$isrcv($e$)) $\Rightarrow$ (sub{-}es{-}sender(${\it es}$;${\it dom}$;$e$) $\in$ \{$e$:E$\mid$ $\uparrow$(${\it dom}$($e$))\} ))